<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>VerifyProofs</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="VerifyProofs";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li>Next Class</li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/VerifyProofs.html" target="_top">Frames</a></li>
<li><a href="VerifyProofs.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.verify</div>
<h2 title="Class VerifyProofs" class="title">Class VerifyProofs</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.verify.VerifyProofs</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>All Implemented Interfaces:</dt>
<dd><a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">VerifyProofs</span>
extends java.lang.Object
implements <a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></pre>
<div class="block">VerifyProofs implements the proof verification process described in
 Metamath(dot)pdf.
 <p>
 It also has a new feature, verifying a syntax RPN as if it were a proof (in a
 sense, Stmt.exprRPN is a proof, a proof that Stmt.formula can be generated
 using the grammar embodied in the Metamath file...) The purpose of this
 feature is primarily to test the grammatical parser's output -- a
 double-check of the results.
 <p>
 The code is optimized for batch processing of a large number of proofs, one
 after the other.
 <p>
 The main "optimization" was to re-use arrays instead of allocating them for
 each proof. The arrays are initially allocated at a size that fits set.mm,
 which has some massive proofs. If an ArrayIndexOutOfBounds exception is
 detected, the arrays are reallocated with a larger size (an upper limit halts
 this process), and a "retry" is performed.
 <p>
 VerifyProofs uses class SubstMapEntry which is a simple data structure that
 should probably be an inner class of VerifyProofs. Other clean-ups are
 probably at hand for reworking this *thing*. One thing is sure, the error
 messages provided by VerifyProofs are much less helpful than those from
 metamath.exe -- but, on the other hand, since Proof Assistant is the best way
 to create proofs, a proof error in an existing file should be rare (creating
 a Metamath proof by hand is like writing assembler code.)
 <p>
 FYI, here is the basic verification algorithm, which leaves out the ugly
 details of disjoint variable restrictions and substitutions:
 <p>
 
 <pre>
     1. init proof work stack, etc.
     2. loop through theorem proof array, for each proof[] step:
        - if null, exception ==> proof incomplete
        - if stmt is a Hyp, ==> push stmt.formula onto stack
        - else if stmt.mandFrame.hypArray.length = zero
              ==> push stmt.formula onto stack
                  (see ccau, for ex.)
        - else (assertion w/hyp):
             findVarSubstMap for assertion
             if notfnd ==> exception...various
             else,
                 - check DjVars restrictions
                 - pop 'n' entries from stack
                     ('n' = nbr of mand hyps)
                 - throw exception if stack underflow!
                 - push substituted assertion formula onto stack.
     3. if stack has more than one entry left,
            ==>exception, > 1 stack entry left, disproved!
     4. if stack entry not equal to stmt to be proved formula
            ==>exception, last entry not equal! disproved!
     5. ok! proved.
 
 </pre></div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../mmjProofVerification.html"> More on Proof
      Verification</a>, 
<a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/VerifyProofs.html#VerifyProofs()">VerifyProofs</a></strong>()</code>
<div class="block">Constructor - default.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#convertRPNToFormula(mmj.lang.ParseTree.RPNStep[], java.lang.String)">convertRPNToFormula</a></strong>(<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;formulaRPN,
                   java.lang.String&nbsp;stepLabelForMessages)</code>
<div class="block">Generate Formula from RPN.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#getPExprHighwater()">getPExprHighwater</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify">ProofDerivationStepEntry</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#getProofDerivationSteps(mmj.lang.Theorem, boolean, boolean, mmj.lang.Cnst)">getProofDerivationSteps</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem,
                       boolean&nbsp;exportFormatUnified,
                       boolean&nbsp;hypsRandomized,
                       <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;provableLogicStmtTyp)</code>
<div class="block">Builds and returns an ArrayList of proof steps for export via the Proof
 Assistant.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#getPStackHighwater()">getPStackHighwater</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#getSubstHighwater()">getSubstHighwater</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#raiseVerifyException(java.lang.String, java.lang.String, java.lang.String, java.lang.Object...)">raiseVerifyException</a></strong>(java.lang.String&nbsp;stepNbrIndexString,
                    java.lang.String&nbsp;stepLabel,
                    java.lang.String&nbsp;errmsg,
                    java.lang.Object...&nbsp;args)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#verifyAllExprRPNAsProofs(mmj.lang.Messages, java.util.Map)">verifyAllExprRPNAsProofs</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                        java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl)</code>
<div class="block">Verify all Statements' grammatical parse RPNs.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#verifyAllProofs(mmj.lang.Messages, java.util.Map)">verifyAllProofs</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
               java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl)</code>
<div class="block">Verify all proofs in Statement Table.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#verifyDerivStepDjVars(java.lang.String, java.lang.String, mmj.lang.Assrt, mmj.lang.ParseNode[], mmj.lang.ScopeFrame, boolean, boolean, java.util.List)">verifyDerivStepDjVars</a></strong>(java.lang.String&nbsp;derivStepNbr,
                     java.lang.String&nbsp;derivStepStmtLabel,
                     <a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&nbsp;derivStepRef,
                     <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;derivStepAssrtSubst,
                     <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;derivStepComboFrame,
                     boolean&nbsp;djVarsSoftErrorsIgnore,
                     boolean&nbsp;djVarsSoftErrorsGenerateNew,
                     java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;softDjVarsErrorList)</code>
<div class="block">Verify that a single proof derivation step does not violate the Distinct
 Variable Restrictions of the step's Ref assertion.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#verifyDerivStepProof(java.lang.String, mmj.lang.Formula, mmj.lang.ParseTree, mmj.lang.ScopeFrame)">verifyDerivStepProof</a></strong>(java.lang.String&nbsp;derivStepStmtLabel,
                    <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;derivStepFormula,
                    <a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;derivStepProofTree,
                    <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;derivStepComboFrame)</code>
<div class="block">Verify a single proof derivation step.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#verifyExprRPNAsProof(mmj.lang.Stmt)">verifyExprRPNAsProof</a></strong>(<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;exprRPNStmt)</code>
<div class="block">Verify grammatical parse RPN as if it were a proof.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/VerifyProofs.html#verifyOneProof(mmj.lang.Theorem)">verifyOneProof</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</code>
<div class="block">Verify a single proof.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="VerifyProofs()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>VerifyProofs</h4>
<pre>public&nbsp;VerifyProofs()</pre>
<div class="block">Constructor - default.</div>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="verifyAllProofs(mmj.lang.Messages, java.util.Map)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyAllProofs</h4>
<pre>public&nbsp;void&nbsp;verifyAllProofs(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                   java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl)</pre>
<div class="block">Verify all proofs in Statement Table.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/ProofVerifier.html#verifyAllProofs(mmj.lang.Messages, java.util.Map)">verifyAllProofs</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object for output error messages.</dd><dd><code>stmtTbl</code> - Statement Table (map).</dd></dl>
</li>
</ul>
<a name="verifyOneProof(mmj.lang.Theorem)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyOneProof</h4>
<pre>public&nbsp;java.lang.String&nbsp;verifyOneProof(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</pre>
<div class="block">Verify a single proof.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/ProofVerifier.html#verifyOneProof(mmj.lang.Theorem)">verifyOneProof</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>theorem</code> - Theorem object reference.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String error message if error(s), or null.</dd></dl>
</li>
</ul>
<a name="verifyAllExprRPNAsProofs(mmj.lang.Messages, java.util.Map)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyAllExprRPNAsProofs</h4>
<pre>public&nbsp;void&nbsp;verifyAllExprRPNAsProofs(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                            java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl)</pre>
<div class="block">Verify all Statements' grammatical parse RPNs.
 <p>
 Note: even VarHyp and Syntax Axioms are assigned default RPN's, so this
 should work -- unless there are errors in the Metamath file, or in the
 grammar itself.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/ProofVerifier.html#verifyAllExprRPNAsProofs(mmj.lang.Messages, java.util.Map)">verifyAllExprRPNAsProofs</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object for output error messages.</dd><dd><code>stmtTbl</code> - Statement Table (map).</dd></dl>
</li>
</ul>
<a name="verifyExprRPNAsProof(mmj.lang.Stmt)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyExprRPNAsProof</h4>
<pre>public&nbsp;java.lang.String&nbsp;verifyExprRPNAsProof(<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;exprRPNStmt)</pre>
<div class="block">Verify grammatical parse RPN as if it were a proof.
 <p>
 Note: even VarHyp and Syntax Axioms are assigned default RPN's, so this
 should work -- unless there are errors in the Metamath file, or in the
 grammar itself.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/ProofVerifier.html#verifyExprRPNAsProof(mmj.lang.Stmt)">verifyExprRPNAsProof</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>exprRPNStmt</code> - Stmt with RPN to verify.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String error message if error(s), or null.</dd></dl>
</li>
</ul>
<a name="verifyDerivStepProof(java.lang.String, mmj.lang.Formula, mmj.lang.ParseTree, mmj.lang.ScopeFrame)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyDerivStepProof</h4>
<pre>public&nbsp;java.lang.String&nbsp;verifyDerivStepProof(java.lang.String&nbsp;derivStepStmtLabel,
                                    <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;derivStepFormula,
                                    <a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;derivStepProofTree,
                                    <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;derivStepComboFrame)</pre>
<div class="block">Verify a single proof derivation step.
 <p>
 Note: the "comboFrame" contains the mandatory and optional information as
 a matter of convenience. The "optional" information is kept separate in
 Metamath because it needs to be available in Proof Verifier (and
 elsewhere), but must not be used when the Assertion is referenced in a
 proof (especially not be pushed onto the stack!)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>derivStepStmtLabel</code> - label + "Step" + step number</dd><dd><code>derivStepFormula</code> - formula of proof step</dd><dd><code>derivStepProofTree</code> - step proof tree.</dd><dd><code>derivStepComboFrame</code> - MandFrame for step.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String error message if error(s), or null.</dd></dl>
</li>
</ul>
<a name="verifyDerivStepDjVars(java.lang.String, java.lang.String, mmj.lang.Assrt, mmj.lang.ParseNode[], mmj.lang.ScopeFrame, boolean, boolean, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyDerivStepDjVars</h4>
<pre>public&nbsp;java.lang.String&nbsp;verifyDerivStepDjVars(java.lang.String&nbsp;derivStepNbr,
                                     java.lang.String&nbsp;derivStepStmtLabel,
                                     <a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&nbsp;derivStepRef,
                                     <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;derivStepAssrtSubst,
                                     <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;derivStepComboFrame,
                                     boolean&nbsp;djVarsSoftErrorsIgnore,
                                     boolean&nbsp;djVarsSoftErrorsGenerateNew,
                                     java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;softDjVarsErrorList)</pre>
<div class="block">Verify that a single proof derivation step does not violate the Distinct
 Variable Restrictions of the step's Ref assertion.
 <p>
 The main complication here is converting the parse subtrees that comprise
 the variable substitutions into the form required by method
 checkDjVars().
 <p>
 Note: the "comboFrame" contains the mandatory and optional information as
 a matter of convenience. The "optional" information is kept separate in
 Metamath because it needs to be available in Proof Verifier (and
 elsewhere), but must not be used when the Assertion is referenced in a
 proof (especially not be pushed onto the stack!)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>derivStepNbr</code> - string, may equal "qed"</dd><dd><code>derivStepStmtLabel</code> - label + "Step" + step number</dd><dd><code>derivStepRef</code> - Assertion justifying the step</dd><dd><code>derivStepAssrtSubst</code> - array of substitution subtrees</dd><dd><code>derivStepComboFrame</code> - MandFrame for step.</dd><dd><code>djVarsSoftErrorsIgnore</code> - whether to ignore soft DjVars errors</dd><dd><code>djVarsSoftErrorsGenerateNew</code> - whether to generate missing DjVars
            restrictions</dd><dd><code>softDjVarsErrorList</code> - the output list of violated DjVars</dd>
<dt><span class="strong">Returns:</span></dt><dd>String error message if error(s), or null.</dd></dl>
</li>
</ul>
<a name="getProofDerivationSteps(mmj.lang.Theorem, boolean, boolean, mmj.lang.Cnst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getProofDerivationSteps</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify">ProofDerivationStepEntry</a>&gt;&nbsp;getProofDerivationSteps(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem,
                                                               boolean&nbsp;exportFormatUnified,
                                                               boolean&nbsp;hypsRandomized,
                                                               <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;provableLogicStmtTyp)
                                                                 throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Builds and returns an ArrayList of proof steps for export via the Proof
 Assistant.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theorem</code> - the theorem whose proof will be exported</dd><dd><code>exportFormatUnified</code> - set to true if proof step label is output on
            each step (else, it is only output on Logical Hypothesis
            steps.)</dd><dd><code>hypsRandomized</code> - set to true if proof step hyps should be rearranged
            in random order (a testing feature.)</dd><dd><code>provableLogicStmtTyp</code> - type code of proof derivation steps to
            return.</dd>
<dt><span class="strong">Returns:</span></dt><dd>List of ProofDerivationStepEntry objects.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if the proof is invalid.</dd></dl>
</li>
</ul>
<a name="raiseVerifyException(java.lang.String, java.lang.String, java.lang.String, java.lang.Object...)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>raiseVerifyException</h4>
<pre>public&nbsp;void&nbsp;raiseVerifyException(java.lang.String&nbsp;stepNbrIndexString,
                        java.lang.String&nbsp;stepLabel,
                        java.lang.String&nbsp;errmsg,
                        java.lang.Object...&nbsp;args)
                          throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<dl><dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code></dd></dl>
</li>
</ul>
<a name="getPStackHighwater()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getPStackHighwater</h4>
<pre>public&nbsp;int&nbsp;getPStackHighwater()</pre>
</li>
</ul>
<a name="getPExprHighwater()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getPExprHighwater</h4>
<pre>public&nbsp;int&nbsp;getPExprHighwater()</pre>
</li>
</ul>
<a name="getSubstHighwater()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSubstHighwater</h4>
<pre>public&nbsp;int&nbsp;getSubstHighwater()</pre>
</li>
</ul>
<a name="convertRPNToFormula(mmj.lang.ParseTree.RPNStep[], java.lang.String)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>convertRPNToFormula</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;convertRPNToFormula(<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;formulaRPN,
                          java.lang.String&nbsp;stepLabelForMessages)</pre>
<div class="block">Generate Formula from RPN.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>formulaRPN</code> - to be converted to a Formula</dd><dd><code>stepLabelForMessages</code> - used for abend message :)</dd>
<dt><span class="strong">Returns:</span></dt><dd>Formula generated from RPN</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li>Next Class</li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/VerifyProofs.html" target="_top">Frames</a></li>
<li><a href="VerifyProofs.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
